SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Spécification de JavaScript</title>

</head>

<h1 id="firstHeading" class="firstHeading mw-first-heading">Spécification de JavaScript</h1>

</header>

</div>

<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="fr" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="fr" dir="ltr">La spécification d'un langage est une définition de la syntaxe et de la sémantique du langage. Cette définition est en général un ensemble de règles syntaxiques définies dans une grammaire.

Initialement dédiés au partage de contenus statiques sur Internet, les sites web sont devenus de véritables applications accessibles à partir de n'importe quel navigateur.

Afin de rendre les sites plus interactifs et dynamiques, il a été nécessaire de mettre en place des langages de script tel que l'<a href="ActionScript" title="ActionScript">ActionScript</a> ou le <a href="JavaScript" title="JavaScript">JavaScript</a>. Ce dernier est actuellement le langage le plus utilisé pour les applications côté client, c'est-à-dire sur le navigateur.

L'<a href="ECMAScript" title="ECMAScript">ECMAScript</a> a vu le jour en 1997 dans le but d'uniformiser l'interprétation de ces différents <a href="Langage_de_script" title="Langage de script">langages de script</a>. Cette spécification décrit la syntaxe et la sémantique que ces langages doivent respecter, sous forme de phrases littérales. Ces définitions étant sujettes a interprétation, on a vu apparaître des divergences d'un langage, ou d'une de ses implémentations, à l'autre. La formalisation de cette spécification EcmaScript permettrait de lisser ces différences d'interprétation.

<div class="mw-heading mw-heading2"><h2 id="Motivations">Motivations</h2></div>

La norme ECMAscript ne décrit pas le comportement à adopter par JavaScript de façon précise du fait que les règles sont définies avec des phrases littérales. En effet, chaque description de la spécification peut être comprise et interprétée différemment, ce qui a mené à l'apparition de divers interpréteurs JavaScript, ou même encore de primitives spécifiques aux <a href="Moteur_de_rendu_HTML" class="mw-redirect" title="Moteur de rendu HTML">moteurs</a> de certains navigateurs, notamment entre <a href="Internet_Explorer" title="Internet Explorer">Internet Explorer</a> et <a href="Mozilla_Firefox" title="Mozilla Firefox">Mozilla Firefox</a><a href="#cite_note-1">[1]</a>.

Cette différence d'interprétation entre Internet Explorer et les autres navigateurs provient du fait que lors de la création du JavaScript par <a href="Brendan_Eich" title="Brendan Eich">Brendan Eich</a> en 1995, <a href="Microsoft" title="Microsoft">Microsoft</a> a développé sa propre version<a href="#cite_note-2">[2]</a> avant que la norme EcmaScript apparaisse.

Ceci est la raison pour laquelle un script fonctionnant correctement sous Internet Explorer ne fonctionnera pas forcément sur un autre navigateur. Dans le but d'assurer une compatibilité optimale entre les différents navigateurs, il est nécessaire de définir une spécification formelle afin que tous les interpréteurs acceptent la même syntaxe.

De plus, le <a href="JavaScript" title="JavaScript">JavaScript</a> possède des vulnérabilités, quant au bon déroulement d'un programme, dues à certains cas non décrits dans la norme <a href="ECMAScript" title="ECMAScript">ECMAScript</a>. Prenons par exemple le cas de l'opérateur <code>typeof</code> : la norme ne décrit pas explicitement quel comportement adopter si l'évaluation de l'expression unitaire provoque une erreur, laissant la possibilité ici d'un comportement variable selon les implémentations<a href="#cite_note-3">[3]</a>. Il est ainsi nécessaire aux analyseurs de gérer ce genre de problèmes. Les différentes interprétations n'assurent donc pas un comportement uniforme des programmes JavaScript, c'est pourquoi plusieurs recherches se portent sur la formalisation de ce langage.

<div class="mw-heading mw-heading2"><h2 id="Approches">Approches</h2></div>

On relève dans la <a href="Communaut%C3%A9_scientifique" title="Communauté scientifique">communauté scientifique</a> au moins 3 approches sur cette question.

<div class="mw-heading mw-heading3"><h3 id="λJS[4]_:_l'essence_de_JavaScript[5]">λJS<a href="#cite_note-4">[4]</a> : l'essence de JavaScript<a href="#cite_note-5">[5]</a></h3></div>

Cette approche part de deux constats : d'une part, le JavaScript n'est pas sécurisé à cause d'une sémantique non conventionnelle ; d'autre part, le langage est trop complexe pour être testé par des outils de tests standard. C'est sur ces deux points que se sont portés les travaux de Arjun Guha, Claudiu Saftoiu et Shriram Krishnamurthi.

Leur premier travail a été de concevoir un noyau, nommé λJS, qui ne contient que les fonctions essentielles du langage, sorte de sous-ensemble complet de JavaScript. Bien sûr, le fait de ne garder que l'essence du langage fait que beaucoup de <a href="Sucre_syntaxique" title="Sucre syntaxique">sucre syntaxique</a> n'existe plus. Prenons, par exemple, l'<a href="Mise_en_%C5%93uvre" title="Mise en œuvre">implémentation</a> des objets, où certaines syntaxes ont été supprimées, au privilège d'une seule lorsque plusieurs sont envisageables. Afin d'accéder à l'attribut <code>x</code> d'un objet <code>Y</code>, il est normalement possible d'écrire <code>Y['x']</code> ou <code>Y.x</code>. Cependant, λJS ne possède que l'écriture <code>Y['x']</code> et n'implémente pas d'écriture alternative afin de garder le noyau de langage le plus petit possible. Une autre modification majeure est la disparation de l'utilisation implicite du <code>this</code>. En effet, lorsque l'on utilise le mot clé <code>this</code>, le programme fait référence à l'objet sur lequel est appelée la fonction. Toutefois, ce paramètre est implicite, il n'est donc pas nécessaire de le renseigner lors de l'appel de la méthode d'un objet, ce qui n'est pas le cas avec λJS. Ils ont ainsi fait disparaître un grand nombre de <a href="Sucre_syntaxique" title="Sucre syntaxique">sucres syntaxiques</a> dans le but de minimiser l'implémentation des fonctions pour permettre plus facilement la vérification d'un programme.

Cependant, afin de faire accepter leur noyau par les autres développeurs, il est nécessaire pour eux de prouver que n'importe quel programme écrit en JavaScript peut être réduit en un programme basé sur λJS. Pour réaliser leurs tests, l'équipe s'est basée sur trois implémentations de Javascript : <a href="SpiderMonkey" title="SpiderMonkey">SpiderMonkey</a> (Firefox), <a href="V8_(moteur_JavaScript)" title="V8 (moteur JavaScript)">V8</a> (Chrome), et <a href="Rhino_(moteur_JavaScript)" title="Rhino (moteur JavaScript)">Rhino</a> (implémentation en Java). Ils ont transformé différents programmes compatibles sur ces implémentations vers un programme λJS, et ont ensuite vérifié que la sortie du nouveau programme correspond à celle de la version d'origine. Afin de couvrir un maximum de cas, les programmes sont un échantillon important de la série de test JavaScript de Mozilla<a href="#cite_note-6">[6]</a>. Les tests ont été concluants : l'intégralité de la série de tests produit exactement le même résultat que les trois autres implémentations.

L'objectif final étant de fournir un langage sûr, il est nécessaire de fournir un outil permettant de vérifier ce résultat. Le λJS étant une implémentation simplifiée du JavaScript, et étant donné qu'un programme peut être réduit en λJS, il est nécessaire de montrer que λJS est sûr. Pour prouver ceci, ils ont décomposé chaque propriété en sous-problèmes. Pour illustrer, prenons le cas de l'addition : ils jugent qu'une addition <code>e1 + e2</code> est sûre si les expressions <code>e1</code> et <code>e2</code> sont sûres. En posant plusieurs <a href="Lemme_(linguistique)" title="Lemme (linguistique)">lemmes</a>, ils démontrent que l'addition est sûre et qu'elle peut être incluse dans le λJS. En appliquant cette démarche sur plusieurs éléments du langage, ils ont réussi à inclure un grand nombre de fonctionnalités à leur noyau en le gardant sûr. Ceci a permis en 2012 de définir le λJS comme base pour le langage JavaScript par ECMAScript 6<a href="#cite_note-7">[7]</a>, toutefois cette version n'est pas encore totalement supportée par tous les navigateurs<a href="#cite_note-8">[8]</a>.

<div class="mw-heading mw-heading3"><h3 id="SAFE_:_une_autre_specification_pour_EcmaScript[9]">SAFE : une autre specification pour EcmaScript<a href="#cite_note-9">[9]</a></h3></div>

SAFE<a href="#cite_note-10">[10]</a> (Scalable <a href="Framework" title="Framework">Framework</a> Analysis for ECMAScript) est un projet mené par le groupe de recherche en <a href="Langage_de_programmation" title="Langage de programmation">langage de programmation</a> de l'Institut supérieur coréen des sciences et technologies (<a href="KAIST" title="KAIST">KAIST</a>).

Tout comme le papier précédent, l'équipe se penche ici sur le constat que la spécification informelle du langage rend celui-ci sujet à interprétation. L'équipe relève également que les différents moteurs Javascript ne sont pas assez documentés, rendant leur compréhension et leur modification difficile. Ceci était le cas avec λJS qu'ils ont souhaité utiliser : ils ont jugé que la documentation concernant la réduction du Javascript en leur noyau n'était pas assez détaillée. C'est en partant de ces deux propositions qu'ils ont débuté le projet SAFE qui a pour but d'améliorer l'analyse d'un programme Javascript ainsi que de fournir un outil documenté pour la recherche.

SAFE est développé à destination de la communauté de recherche en JavaScript, c'est un projet <a href="Open_source" title="Open source">open-source</a> dont le code est accessible en ligne<a href="#cite_note-11">[11]</a>. L'implémentation est réalisée en <a href="Java_(technique)" title="Java (technique)">Java</a> et en <a href="Scala_(langage)" title="Scala (langage)">Scala</a>.

Comparé à l'approche de λJS, l'équipe ne s'est pas contentée de réduire un maximum de langage afin de fournir une spécification simplifiée mais a préféré réaliser une spécification de l'ensemble du langage. C'est dans ce sens qu'ils ont défini une spécification sur chaque niveau de représentation d'un programme Javascript.

<div class="mw-heading mw-heading4"><h4 id="L'arbre_de_syntaxe_abstrait_:_AST">L'arbre de syntaxe abstrait : AST</h4></div>

Afin de réaliser leur framework, il a été dans un premier temps nécessaire de transformer le code Javascript en un code facilement analysable.

Pour ce faire, le framework se base sur 3 niveaux de représentation d'un programme Javascript. La première représentation (qui est la plus proche du <a href="Code_source" title="Code source">code source</a>) est un AST (<a href="Arbre_syntaxique_abstrait" class="mw-redirect" title="Arbre syntaxique abstrait">Arbre syntaxique abstrait</a>). Afin d'obtenir l'AST correspondant au code source analysé, l'équipe s'est intéressée aux parsers JavaScript existants (<a href="ANTLR" title="ANTLR">ANTLR</a><a href="#cite_note-12">[12]</a>, les combinateurs de parseur de Scala<a href="#cite_note-13">[13]</a>, <a href="Rhino_(moteur_JavaScript)" title="Rhino (moteur JavaScript)">Rhino</a>, <a href="SpiderMonkey" title="SpiderMonkey">SpiderMonkey</a>, Closure Tools<a href="#cite_note-14">[14]</a> de <a href="Google" title="Google">Google</a>, JSConTest<a href="#cite_note-15">[15]</a>, ou encore JSure<a href="#cite_note-16">[16]</a>) sans trouver entière satisfaction. Elle a finalement utilisé l'outil de génération Rats! se trouvant dans le projet eXTensible Compiler<a href="#cite_note-17">[17]</a> développé par une équipe de New York. Elle fournit à Rats! une <a href="Forme_de_Backus-Naur" title="Forme de Backus-Naur">grammaire de style BNF</a> dont voici l'extrait<a href="#cite_note-18">[18]</a> concernant les instructions de boucle (l'indentation représente une relation de sous-classe) :

<div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre> /**

* SourceElement ::= Stmt

abstract Stmt();

/**

* Stmt ::= do Stmt while ( Expr ) ;

DoWhile(Stmt body, Expr cond);

/**

* Stmt ::= while ( Expr ) Stmt

While(Expr cond, Stmt body);

/**

* Stmt ::= for ( Expr? ; Expr? ; Expr? ) Stmt

For(Option<Expr> init, Option<Expr> cond,

Option<Expr> action, Stmt body);

/**

* Stmt ::= for ( lhs in Expr ) Stmt

ForIn(LHS lhs, Expr expr, Stmt body);

/**

* Stmt ::= for ( var VarDecl(, VarDecl)* ;

Expr? ; Expr? ) Stmt

ForVar(List<VarDecl> vars, Option<Expr> cond,

Option<Expr> action, Stmt body);

/**

* Stmt ::= for ( var VarDecl in Expr ) Stmt

ForVarIn(VarDecl var, Expr expr, Stmt body);

</pre></div>

Rats! génère alors un parser JavaScript en langage <a href="Java_(langage)" title="Java (langage)">Java</a>, qui couplé à ASTGen<a href="#cite_note-19">[19]</a>, qui génère les classes Java représentant l'AST à partir d'une description fournie, va permettre de transformer le code JavaScript en représentation intermédiaire.

<div class="mw-heading mw-heading4"><h4 id="La_représentation_intermédiaire_:_IR">La représentation intermédiaire : IR</h4></div>

Dans un second temps, le framework transforme l'AST en une représentation intermédiaire IR qui permet de fournir une spécification de chaque fonctionnalité du langage Javascript définie par ECMAScript. Par exemple, chaque fonction possède au moins l'argument <code>this</code> afin de respecter cette norme. C'est cette représentation qui est utilisée pour l'évaluation du programme par un interpréteur. C'est à ce niveau qu'intervient SAFE en fournissant une spécification formelle et une implémentation de chaque fonctionnalité.

Grammaire de JavaScript IR<a href="#cite_note-20">[20]</a> :

<pre> p ::= s*

s ::= x = e

| x = delete x

| x = delete x [x]

| x = {(m,)* }

| x = [(e,)* ]

| x = x(x(, x)?)

| x = new x((x,)* )

| x = function f(x, x) { s* }

| function f(x, x) { s* }

| x = eval(e)

| x [x] = e

| break x

| return e?

| with (x) s

| x : { s }

| var x

| throw e

| s*

| if (e) then s (else s)?

| while(e) s

| try { s } (catch (x){ s })? (finally { s })?

| (s* )

e ::= e ⊗ e

| ɵ e

| x [e]

| x

| this

| num

| str

| true

| false

| undefined

| null

m ::= x : x

| get f(x, x) { s* }

| set f(x, x) { s* }

⊗ ::= | | & | ^ | << | >> | >>> | + | - | * | / | % | == | != | === | !== | < | > | <= | >= | instanceof | in

ɵ ::= ~ | ! | + | - | void | typeof

</pre>

<div class="mw-heading mw-heading4"><h4 id="Le_graphe_de_flot_de_contrôle_:_CFG">Le <a href="Graphe_de_flot_de_contr%C3%B4le" title="Graphe de flot de contrôle">graphe de flot de contrôle</a> : CFG</h4></div>

Le troisième niveau de représentation est le CFG (Graphe de flot de contrôle) qui est utilisé uniquement pour l'analyse des performances. Afin de générer ce graphe, le projet utilise CFGBuilder qui est un composant du compilateur Polyglot. Ce programme prend en paramètre une représentation intermédiaire et génère un graphe correspondant qui pourra ensuite être analysé par le framework afin de réaliser plusieurs analyses.

Un exemple de transformation du code JavaScript au graphe de contrôle de flot en passant par la représentation intermédiaire, proposé dans le paragraphe 3.3 dans la publication présentant SAFE<a href="#cite_note-21">[21]</a>, illustre bien le résultat obtenu à ce stade.

<div class="mw-heading mw-heading4"><h4 id="Applications">Applications</h4></div>

Leur framework est disponible au public<a href="#cite_note-22">[22]</a>. Afin de permettre l'utilisation de leur projet par le plus grand nombre, SAFE fournit, en plus de la spécification et d'une documentation fournie, une implémentation des différentes fonctionnalités. Ceci permet d'utiliser leurs recherches plus facilement que les autres projets qui n'ont pas ou peu de documentation.

Les 3 niveaux de représentation du code JavaScript (AST, IR, CFG) rendent SAFE plus flexible, évolutif, et connectable, proposant ainsi un outil puissant dans la recherche et le développement de JavaScript.

<div class="mw-heading mw-heading3"><h3 id="JSCert_:_une_spécification_mécanisée_et_sûre_de_JavaScript[23]">JSCert : une spécification mécanisée et sûre de JavaScript<a href="#cite_note-23">[23]</a></h3></div>

"Le projet JSCert a pour but de vraiment comprendre JavaScript", annonce le site du projet. Une équipe de chercheurs des laboratoires de l'INRIA et de l'Imperial College London se sont intéressés à la nécessité de clarifier les ambiguïtés liées à la longueur et aux nombreux recoins du standard ECMAScript.

<div class="mw-heading mw-heading4"><h4 id="JSCert">JSCert</h4></div>

JSCert est une spécification mécanisée du standard ECMAScript, écrite dans l'assistant interactif de preuve <a href="Rocq_(logiciel)" title="Rocq (logiciel)">Rocq</a>, conçue pour être la plus proche de la norme ECMAScript5<a href="#cite_note-24">[24]</a>. Elle se base sur le développement en 2008, mené par Sergio Maffeis, d'une sémantique de description formelle du comportement complet de JavaScript<a href="#cite_note-25">[25]</a> suivant fidèlement ECMAScript3, à l'exception des parties ambiguës de ce standard. Cette formalisation se limite au cœur du langage JavaScript.

<div class="mw-heading mw-heading4"><h4 id="JSRef">JSRef</h4></div>

En parallèle a été développé JSRef, un interpréteur exécutable de référence, certifié dans le respect de JSCert, et testé en utilisant la suite de tests de confirmité d'ECMAScript, test262<a href="#cite_note-26">[26]</a>.

JSCert n'est pas directement utilisable, de par sa conception : c'est une définition inductive à destination du développement de preuves de sûreté, qui compense l'imprécision concernant les fonctionnalités dépendantes de l'implémentation dans ECMAScript5. En tant que spécification Rocq calculable, on en a extrait automatiquement le code <a href="OCaml" title="OCaml">OCaml</a> correspondant, obtenant ainsi l'interpréteur JSRef. Celui-ci respecte la norme ECMAScript5 autant qu'il était possible de la formaliser par JSCert.

<div class="mw-heading mw-heading4"><h4 id="De_ECMAScript_à_JSRef">De ECMAScript à JSRef</h4></div>

La vérification de JSCert dans cette sémantique mécanisée est dû à sa proximité avec la norme ECMAScript5 : la prose anglaise de celle-ci et les règles formelles qui en découlent peuvent être mises côte-à-côte, chaque ligne de <a href="Pseudo-code" title="Pseudo-code">pseudo-code</a> correspondant à une ou deux règles formelles de JSCert. JSRef se vérifie par le mécanisme automatique par lequel il est extrait de JSCert.

Le pseudo-code<a href="#cite_note-27">[27]</a> correspondant à la <a href="Boucle_while" title="Boucle while">boucle while</a> dans ECMAScript5 :

<div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre> 1. Let V = empty.

2. Repeat

a. Let exprRef be the result of evaluating Expression.

b. If ToBoolean(GetValue(exprRef)) is false, return (normal,V,empty).

c. Let stmt be the result of evaluating Statement.

d. If stmt.value is not empty, let V = stmt.value.

e. If stmt.type is not continue || stmt.target is not in the current label set, then

i. If stmt.type is break and stmt.target is in the current label set, then return (normal,V,empty).

ii. If stmt is an abrupt completion, return stmt.

</pre></div>

La sémantique JSCert implémentée dans Rocq correspondant à la boucle while, et traduisant la sémantique définie dans la publication de JSCert<a href="#cite_note-28">[28]</a> :

<div class="mw-highlight mw-highlight-lang-ocaml mw-content-ltr" dir="ltr"><pre> (* Step 1: red_while_1 *)

| red_stat_while : forall S C labs e1 t2 o,

red_stat S C (stat_while_1 labs e1 t2 resvalue_empty) o ->

red_stat S C (stat_while labs e1 t2) o

(* Steps 2a and 2b: red_while_2a_2b *)

| red_stat_while_1 : forall S C labs e1 t2 rv y1 o,

red_spec S C (spec_expr_get_value_conv spec_to_boolean e1) y1 ->

red_stat S C (stat_while_2 labs e1 t2 rv y1) o ->

red_stat S C (stat_while_1 labs e1 t2 rv) o

(* Step 2b False: red_while_2b'_false *)

| red_stat_while_2_false : forall S0 S C labs e1 t2 rv,

red_stat S0 C (stat_while_2 labs e1 t2 rv (vret S false)) (out_ter S rv)

(* Step 2b True and 2c: red_while_2b'_true_2c *)

| red_stat_while_2_true : forall S0 S C labs e1 t2 rv o1 o,

red_stat S C t2 o1 ->

red_stat S C (stat_while_3 labs e1 t2 rv o1) o ->

red_stat S0 C (stat_while_2 labs e1 t2 rv (vret S true)) o

(* Step 2d: red_while_2d *)

| red_stat_while_3 : forall rv S0 S C labs e1 t2 rv' R o,

rv' = (If res_value R <> resvalue_empty then res_value R else rv) ->

red_stat S C (stat_while_4 labs e1 t2 rv' R) o ->

red_stat S0 C (stat_while_3 labs e1 t2 rv (out_ter S R)) o

(* Step 2e False: red_while_2e_false *)

| red_stat_while_4_continue : forall S C labs e1 t2 rv R o,

res_type R = restype_continue /\ res_label_in R labs ->

red_stat S C (stat_while_1 labs e1 t2 rv) o ->

red_stat S C (stat_while_4 labs e1 t2 rv R) o

(* Step 2e True: red_while_2e_true *)

| red_stat_while_4_not_continue : forall S C labs e1 t2 rv R o,

~ (res_type R = restype_continue /\ res_label_in R labs) ->

red_stat S C (stat_while_5 labs e1 t2 rv R) o ->

red_stat S C (stat_while_4 labs e1 t2 rv R) o

(* Step 2e i True: red_while_2e_i_true *)

| red_stat_while_5_break : forall S C labs e1 t2 rv R,

res_type R = restype_break /\ res_label_in R labs ->

(* Step 2e i False: red_while_2e_i_false *)

| red_stat_while_5_not_break : forall S C labs e1 t2 rv R o,

~ (res_type R = restype_break /\ res_label_in R labs) ->

red_stat S C (stat_while_6 labs e1 t2 rv R) o ->

(* Step 2e ii True: red_while_2e_ii_true *)

| red_stat_while_6_abort : forall S C labs e1 t2 rv R,

res_type R <> restype_normal ->

(* Step 2e ii False: red_while_2e_ii_false *)

| red_stat_while_6_normal : forall S C labs e1 t2 rv R o,

res_type R = restype_normal ->

red_stat S C (stat_while_1 labs e1 t2 rv) o ->

</pre></div>

La sémantique JSRef de la boucle while<a href="#cite_note-29">[29]</a> :

<div class="mw-highlight mw-highlight-lang-ocaml mw-content-ltr" dir="ltr"><pre>Definition run_stat_while runs S C rv labs e1 t2 : result :=

if_spec (run_expr_get_value runs S C e1) (fun S1 v1 =>

Let b := convert_value_to_boolean v1 in

if b then

if_ter (runs.runs_type_stat S1 C t2) (fun S2 R =>

Let rv' := ifb res_value R != resvalue_empty

then res_value R else rv in

Let loop := fun _ => runs.runs_type_stat_while S2 C rv' labs e1 t2 in

ifb res_type R != restype_continue

|| res_label_in R labs

then (ifb res_type R = restype_break

&& res_label_in R labs

then res_ter S2 rv'

else (ifb res_type R != restype_normal

then res_ter S2 R else loop tt))

else loop tt)

else res_ter S1 rv).

Definition run_stat runs S C t : result :=

match t with

|stat_while ls e1 t2 => runs.runs_type_stat_while S C ls e1 t2 resvalue_empt...

</pre></div>

<div class="mw-heading mw-heading4"><h4 id="Applications_2">Applications</h4></div>

On peut envisager plusieurs utilisations potentielles de JSCert et JSRef :

<ul><li>analyser des morceaux de code JavaScript</li>

<li>vérifier la bonne implémentation d'un compilateur d'un langage de plus haut niveau en JavaScript</li>

<li>comparer l'implémentation d'un interpréteur avec celle de JSRef</li></ul>

On peut imaginer que cette spécification formelle et mécanisée soit intégrée dans une future édition d'ECMAScript.

<div class="mw-heading mw-heading2"><h2 id="Synthèse">Synthèse</h2></div>

<th>

</th>

<th>λJS

</th>

<th>SAFE

</th>

<th>JSCert

</th></tr>

<tr>

<td>Motivation

</td>

<td>Pouvoir tester plus efficacement des programmes

Diminuer la complexité des programmes

</td>

<td>Améliorer l'analyse des programmes

Fournir des outils pour la recherche

</td>

<td>Fournir une représentation formelle de l'ECMASCRIPT

Clarifier ECMAScript en cas de doute sur l'interprétation

Fournir un interpréteur vérifiant qu'un programme respecte cette spécification

</td></tr>

<tr>

<td>Réalisations

</td>

<td>Réalisation d'un noyau minimal de Javascript

Assurer la sureté de ce noyau

Ramener le sucre syntaxique aux fonctions de base

</td>

<td>Fournir une spécification et une implémentation de l'ECMAScript

Convertir l'AST d'un programme Javascript vers une représentation intermédiaire

</td>

<td>Réalisation d'une spécification formelle des fonctionnalités de Javascript

Réalisation d'un interpréteur respectant JSCert

</td></tr>

<tr>

<td>Spécification

effectuée

</td>

<td>Réduction du Javascript en un ensemble de fonction minimale

</td>

<td>Spécification sur chaque niveau de représentation d'un programme Javascript

</td>

<td>Réalisation d'une spécification en Rocq

</td></tr></tbody></table>

<div class="mw-heading mw-heading2"><h2 id="Liens_externes">Liens externes</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Notes_et_références">Notes et références</h3></div>

<li id="cite_note-1"><a href="#cite_ref-1">↑</a> Serge Descombes, « <a rel="nofollow" class="external text" href="http://www.journaldunet.com/developpeur/tutoriel/dht/020911_dom.shtml"><cite style="font-style:normal;">Le Journal du Net - Petit guide de compatibilité des navigateurs web</cite></a> », <time class="nowrap" datetime="2002-09-11" data-sort-value="2002-09-11">11 septembre 2002</time> (consulté le <time class="nowrap" datetime="2014-12-02" data-sort-value="2014-12-02">2 décembre 2014</time>).

</li>

<li id="cite_note-2"><a href="#cite_ref-2">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="https://www.w3.org/community/webed/wiki/A_Short_History_of_JavaScript"><cite style="font-style:normal;" lang="en">A Short History of JavaScript</cite></a> », <time class="nowrap" datetime="2012-06" data-sort-value="2012-06">juin 2012</time> (consulté le <time class="nowrap" datetime="2014-12-09" data-sort-value="2014-12-09">9 décembre 2014</time>).

</li>

<li id="cite_note-3"><a href="#cite_ref-3">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="http://www.ecma-international.org/ecma-262/5.1/#sec-11.4.3"><cite style="font-style:normal;" lang="en">ECMAScript language specification - The typeof Operator</cite></a> », <time class="nowrap" datetime="2011-06" data-sort-value="2011-06">juin 2011</time> (consulté le <time class="nowrap" datetime="2014-12-02" data-sort-value="2014-12-02">2 décembre 2014</time>).

</li>

<li id="cite_note-4"><a href="#cite_ref-4">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="http://orangoo.com/labs/AJS/"><cite style="font-style:normal;" lang="en">The ultra lightweight JavaScript library</cite></a> », sur orangoo.com, <time class="nowrap" datetime="2008-06-21" data-sort-value="2008-06-21">21 juin 2008</time> (consulté le <time class="nowrap" datetime="2015-01-07" data-sort-value="2015-01-07">7 janvier 2015</time>).

</li>

<li id="cite_note-5"><a href="#cite_ref-5">↑</a> <a href="#λJS">Guha, Saftoiu et Krishnamurthi 2010</a>

</li>

<li id="cite_note-6"><a href="#cite_ref-6">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="https://developer.mozilla.org/en-US/docs/Mozilla/QA/Automated_testing"><cite style="font-style:normal;" lang="en">Mozilla automated testing</cite></a> », sur developer.mozilla.org, <time class="nowrap" datetime="2014-09-08" data-sort-value="2014-09-08">8 septembre 2014</time> (consulté le <time class="nowrap" datetime="2014-12-14" data-sort-value="2014-12-14">14 décembre 2014</time>).

</li>

<li id="cite_note-7"><a href="#cite_ref-7">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="http://blog.brownplt.org/2012/04/01/ecma-lambdajs-announcement.html"><cite style="font-style:normal;" lang="en">ECMA Announces Official λJS Adoption</cite></a> », sur blog.brownplt.org,‎ <time class="nowrap" datetime="2012-04-01" data-sort-value="2012-04-01"><abbr class="abbr" title="premier">1er</abbr> avril 2012</time> (consulté le <time class="nowrap" datetime="2014-12-14" data-sort-value="2014-12-14">14 décembre 2014</time>).

</li>

<li id="cite_note-8"><a href="#cite_ref-8">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="https://kangax.github.io/compat-table/es6/"><cite style="font-style:normal;" lang="en">ECMASCRIPT compatibility table</cite></a> », sur kangax.github.io (consulté le <time class="nowrap" datetime="2015-01-07" data-sort-value="2015-01-07">7 janvier 2015</time>).

</li>

</li>

<li id="cite_note-10"><a href="#cite_ref-10">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="http://plrg.kaist.ac.kr/research/safe"><cite style="font-style:normal;" lang="en">KAIST</cite></a> », sur plrg.kaist.ac.kr (consulté le <time class="nowrap" datetime="2014-12-15" data-sort-value="2014-12-15">15 décembre 2014</time>).

</li>

<li id="cite_note-11"><a href="#cite_ref-11">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="http://plrg.kaist.ac.kr/redmine/projects/jsf/repository"><cite style="font-style:normal;" lang="en">KAIST source code</cite></a> », sur plrg.kaist.ac.kr (consulté le <time class="nowrap" datetime="2014-12-15" data-sort-value="2014-12-15">15 décembre 2014</time>).

</li>

<li id="cite_note-12"><a href="#cite_ref-12">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="http://www.antlr.org/"><cite style="font-style:normal;" lang="en">ANTLR</cite></a> » (consulté le <time class="nowrap" datetime="2014-12-16" data-sort-value="2014-12-16">16 décembre 2014</time>).

</li>

<li id="cite_note-13"><a href="#cite_ref-13">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="http://www.scala-lang.org/api/2.10.2/index.html#scala.util.parsing.combinator.Parsers"><cite style="font-style:normal;" lang="en">Scala's parser combinators documentation</cite></a> », sur scala-lang.org (consulté le <time class="nowrap" datetime="2014-12-16" data-sort-value="2014-12-16">16 décembre 2014</time>).

</li>

<li id="cite_note-14"><a href="#cite_ref-14">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="https://developers.google.com/closure"><cite style="font-style:normal;" lang="en">Closure Tools</cite></a> », sur developers.google.com (consulté le <time class="nowrap" datetime="2014-12-16" data-sort-value="2014-12-16">16 décembre 2014</time>).

</li>

<li id="cite_note-15"><a href="#cite_ref-15">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="https://github.com/heidegger/JSConTest"><cite style="font-style:normal;" lang="en">JSConTest</cite></a> », sur github.com (consulté le <time class="nowrap" datetime="2014-12-16" data-sort-value="2014-12-16">16 décembre 2014</time>).

</li>

<li id="cite_note-16"><a href="#cite_ref-16">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="https://github.com/berke/jsure"><cite style="font-style:normal;" lang="en">JSure</cite></a> », sur github.com (consulté le <time class="nowrap" datetime="2014-12-16" data-sort-value="2014-12-16">16 décembre 2014</time>).

</li>

<li id="cite_note-17"><a href="#cite_ref-17">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="http://cs.nyu.edu/rgrimm/xtc/"><cite style="font-style:normal;" lang="en">XTC</cite></a> », sur cs.nyu.edu, <time class="nowrap" datetime="2014-08-17" data-sort-value="2014-08-17">17 août 2014</time> (consulté le <time class="nowrap" datetime="2014-12-15" data-sort-value="2014-12-15">15 décembre 2014</time>).

</li>

<li id="cite_note-18"><a href="#cite_ref-18">↑</a> <a href="#Safe">Lee <abbr class="abbr" title="et alii (« et d’autres »)" lang="la">et al.</abbr> 2012</a>, Fig. 9, <abbr class="abbr" title="page(s)">p.</abbr> 7

</li>

<li id="cite_note-19"><a href="#cite_ref-19">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="http://sourceforge.net/projects/astgen/"><cite style="font-style:normal;" lang="en">ASTGen</cite></a> », sur sourceforge.net (consulté le <time class="nowrap" datetime="2014-12-16" data-sort-value="2014-12-16">16 décembre 2014</time>).

</li>

<li id="cite_note-20"><a href="#cite_ref-20">↑</a> <a href="#Safe">Lee <abbr class="abbr" title="et alii (« et d’autres »)" lang="la">et al.</abbr> 2012</a>, Fig. 4, <abbr class="abbr" title="page(s)">p.</abbr> 4

</li>

<li id="cite_note-21"><a href="#cite_ref-21">↑</a> <a href="#Safe">Lee <abbr class="abbr" title="et alii (« et d’autres »)" lang="la">et al.</abbr> 2012</a>, § 3.3, <abbr class="abbr" title="page(s)">p.</abbr> 5 & 7

</li>

<li id="cite_note-22"><a href="#cite_ref-22">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="https://github.com/sukyoung/safe"><cite style="font-style:normal;" lang="en">SAFE Github</cite></a> », sur github.com, <time class="nowrap" datetime="2014-09-21" data-sort-value="2014-09-21">21 septembre 2014</time> (consulté le <time class="nowrap" datetime="2014-12-14" data-sort-value="2014-12-14">14 décembre 2014</time>).

</li>

<li id="cite_note-23"><a href="#cite_ref-23">↑</a> <a href="#JSCert_ref">Bodin <abbr class="abbr" title="et alii (« et d’autres »)" lang="la">et al.</abbr> 2014</a>, <abbr class="abbr" title="page(s)">p.</abbr> 87-100

</li>

<li id="cite_note-24"><a href="#cite_ref-24">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="http://www.ecma-international.org/ecma-262/5.1/"><cite style="font-style:normal;" lang="en">Standard ECMA-262</cite></a> », sur ecma-international.org (consulté le <time class="nowrap" datetime="2015-01-07" data-sort-value="2015-01-07">7 janvier 2015</time>).

</li>

<li id="cite_note-25"><a href="#cite_ref-25">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="http://jssec.net/semantics/"><cite style="font-style:normal;" lang="en">An Operational Semantics for JavaScript</cite></a> », <time>2008</time> (consulté le <time class="nowrap" datetime="2014-12-15" data-sort-value="2014-12-15">15 décembre 2014</time>),<a href="#OperationalSemantics">Maffeis, Mitchell et Taly 2008</a>, <abbr class="abbr" title="page(s)">p.</abbr> 307-325.

</li>

<li id="cite_note-26"><a href="#cite_ref-26">↑</a> <abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="http://test262.ecmascript.org/"><cite style="font-style:normal;" lang="en">ECMAScript Language test262</cite></a> » (consulté le <time class="nowrap" datetime="2014-12-15" data-sort-value="2014-12-15">15 décembre 2014</time>).

</li>

<li id="cite_note-27"><a href="#cite_ref-27">↑</a> <a href="#JSCert_ref">Bodin <abbr class="abbr" title="et alii (« et d’autres »)" lang="la">et al.</abbr> 2014</a>, Fig. 1, <abbr class="abbr" title="page(s)">p.</abbr> 91

</li>

<li id="cite_note-28"><a href="#cite_ref-28">↑</a> <a href="#JSCert_ref">Bodin <abbr class="abbr" title="et alii (« et d’autres »)" lang="la">et al.</abbr> 2014</a>, Fig. 3, <abbr class="abbr" title="page(s)">p.</abbr> 94

</li>

<li id="cite_note-29"><a href="#cite_ref-29">↑</a> <a href="#JSCert_ref">Bodin <abbr class="abbr" title="et alii (« et d’autres »)" lang="la">et al.</abbr> 2014</a>, Fig. 5, <abbr class="abbr" title="page(s)">p.</abbr> 96

</li>

</ol>

</div>

<div class="mw-heading mw-heading3"><h3 id="Bibliographie">Bibliographie</h3></div>

<abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> Arjun Guha, Claudiu Saftoiu et Shriram Krishnamurthi, « <cite style="font-style:normal" lang="en">The Essence of JavaScript</cite> », ECOOP '10 Proceedings of the 24th European conference on Object-oriented programming,‎ <time class="nowrap" datetime="2010-06-21" data-sort-value="2010-06-21">21 juin 2010</time>, <abbr class="abbr" title="pages">p.</abbr> 126-150 (<a href="International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> 3-642-14106-4 et 978-3-642-14106-5, <a rel="nofollow" class="external text" href="https://cs.brown.edu/~sk/Publications/Papers/Published/gsk-essence-javascript/paper.pdf">lire en ligne</a>)<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=The+Essence+of+JavaScript&rft.jtitle=ECOOP+%2710+Proceedings+of+the+24th+European+conference+on+Object-oriented+programming&rft.aulast=Guha&rft.aufirst=Arjun&rft.au=Saftoiu%2C+Claudiu&rft.au=Krishnamurthi%2C+Shriram&rft.date=2010-06-21&rft.pages=126-150&rft.isbn=3-642-14106-4&rft_id=https%3A%2F%2Fcs.brown.edu%2F~sk%2FPublications%2FPapers%2FPublished%2Fgsk-essence-javascript%2Fpaper.pdf&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ASp%C3%A9cification+de+JavaScript"><div style="margin-left:2em; line-height:1.5;">Brown University</div>

<abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> Hongki Lee, Sooncheol Won, Joonho Jin, Junhee Cho et Sukyoung Ryu, « <cite style="font-style:normal" lang="en">SAFE: Formal Specification and Implementation of a Scalable Analysis Framework for ECMAScript</cite> », FOOL '12 Foundations of Object-Oriented Languages,‎ <time class="nowrap" datetime="2012-10-22" data-sort-value="2012-10-22">22 octobre 2012</time> (<a href="CiteSeerX" title="CiteSeerX">CiteSeerx</a> <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.387.1030">10.1.1.387.1030</a>, <a rel="nofollow" class="external text" href="http://www.cs.uwm.edu/~boyland/fool2012/papers/fool2012_submission_5.pdf">lire en ligne</a>)<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=SAFE%3A+Formal+Specification+and+Implementation+of+a+Scalable+Analysis+Framework+for+ECMAScript&rft.jtitle=FOOL+%2712+Foundations+of+Object-Oriented+Languages&rft.aulast=Lee&rft.aufirst=Hongki&rft.au=Won%2C+Sooncheol&rft.au=Jin%2C+Joonho&rft.au=Cho%2C+Junhee&rft.au=Ryu%2C+Sukyoung&rft.date=2012-10-22&rft_id=http%3A%2F%2Fwww.cs.uwm.edu%2F~boyland%2Ffool2012%2Fpapers%2Ffool2012_submission_5.pdf&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ASp%C3%A9cification+de+JavaScript"><div style="margin-left:2em; line-height:1.5;">KAIST</div>

<abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudžiuniene, Alan Schmitt et Gareth Smith, « <cite style="font-style:normal" lang="en">A Trusted Mechanised JavaScript Specification</cite> », POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,‎ <time class="nowrap" datetime="2014-01-22" data-sort-value="2014-01-22">22 janvier 2014</time> (<a href="International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> 978-1-4503-2544-8, <a href="Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <a rel="nofollow" class="external text" href="https://dx.doi.org/10.1145/2535838.2535876">10.1145/2535838.2535876</a>, <a rel="nofollow" class="external text" href="http://www.doc.ic.ac.uk/~gds/jscert_popl14.pdf">lire en ligne</a>)<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=A+Trusted+Mechanised+JavaScript+Specification&rft.jtitle=POPL+%2714+Proceedings+of+the+41st+ACM+SIGPLAN-SIGACT+Symposium+on+Principles+of+Programming+Languages&rft.aulast=Bodin&rft.aufirst=Martin&rft.au=Chargu%C3%A9raud%2C+Arthur&rft.au=Filaretti%2C+Daniele&rft.au=Gardner%2C+Philippa&rft.au=Maffeis%2C+Sergio&rft.au=Naud%C5%BEiuniene%2C+Daiva&rft.au=Schmitt%2C+Alan&rft.au=Smith%2C+Gareth&rft.date=2014-01-22&rft.isbn=978-1-4503-2544-8&rft_id=info%3Adoi%2F10.1145%2F2535838.2535876&rft_id=http%3A%2F%2Fwww.doc.ic.ac.uk%2F~gds%2Fjscert_popl14.pdf&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ASp%C3%A9cification+de+JavaScript"><div style="margin-left:2em; line-height:1.5;">INRIA & Imperial College London</div>

<abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> Sergio Maffeis, John C. Michell et Ankur Taly, « <cite style="font-style:normal" lang="en">An Operational Semantics for JavaScript</cite> », APLAS '08,‎ <time>2008</time> (<a rel="nofollow" class="external text" href="http://www-cs-students.stanford.edu/~ataly/Papers/aplas08.pdf">lire en ligne</a>)<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=An+Operational+Semantics+for+JavaScript&rft.jtitle=APLAS+%2708&rft.aulast=Maffeis&rft.aufirst=Sergio&rft.au=Michell%2C+John+C.&rft.au=Taly%2C+Ankur&rft.date=2008&rft_id=http%3A%2F%2Fwww-cs-students.stanford.edu%2F~ataly%2FPapers%2Faplas08.pdf&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ASp%C3%A9cification+de+JavaScript">

<div class="mw-heading mw-heading3"><h3 id="Articles_connexes">Articles connexes</h3></div>

<ul><li><a href="JavaScript" title="JavaScript">JavaScript</a></li>

<li><a href="ECMAScript" title="ECMAScript">ECMAScript</a></li></ul>

<ul id="bandeau-portail" class="bandeau-portail"><li> Portail de la programmation informatique </li> </ul></div><div><div class="zim-footer">

Cet article est issu de <a class="external text" title="Dernière modification le 2025-03-15" href="https://fr.wikipedia.org/wiki/?title=Sp%C3%A9cification_de_JavaScript&oldid=223921674">Wikipédia</a>. Sauf mention contraire, le texte est disponible sous <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.fr">Creative Commons Attribution-Share Alike 4.0</a>. Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.

</div>

</div></div>

</div>

</main>

</div>

</body></html>